{-# LANGUAGE TypeFamilies, ConstraintKinds #-}

module RPV where

import TypeBasics (Proxy(..))
import GHC.Prim (Constraint)




type family Con  (rpv :: * -> *) a :: Constraint
type family Inst (rpv :: * -> *) a
class RPV rpv where instantiate :: Con rpv a => rpv a -> Inst rpv a

instantiateAt :: (RPV rpv, Con rpv a) => rpv a -> Proxy a -> Inst rpv a
instantiateAt rpv _ = instantiate rpv





data IdF a = IdF
type instance Con IdF a = ()
type instance Inst IdF a = a -> a
instance RPV IdF where instantiate _ = id
